$\forall$$A$, $B$:Type. AtomFree(Type;$A$) $\Rightarrow$ AtomFree(Type;$B$) $\Rightarrow$ AtomFree(Type;$A$$\rightarrow$$B$)